T, T':Type, f:(TT'), L:(T List), x', y':T'.
x' before y'  map(f;L)  (x,y:T. (x before y  L & f(x) = x' & f(y) = y')) 

latex

Definitions	x:A. B(x), map(f;as), Y, t  T, P  Q, x:A. B(x), P & Q, P  Q, , P  Q, x. t(x), P  Q, A c B, {T}, False, x(s)
Lemmas	all functionality wrt iff, iff wf, l before wf, false wf, iff functionality wrt iff, nil before, exists functionality wrt iff, and functionality wrt iff, map wf, l member wf, cons before, member map